A:Dsys, i, a:Id. Dec(a declared in M(i)) 

latex

Definitions	Dec(P), x  dom(f), KindDeq, locl(a), a:A fp B(a), x. t(x), Knd, MsgA, M(i), P  Q, a declared in M, Valtype(da;k), x:A. B(x), Id, t  T, Dsys
Lemmas	dsys wf, Id wf, msga wf, d-m wf, Knd wf, fpf-trivial-subtype-top, locl wf, Kind-deq wf, fpf-dom wf, decidable assert